the_w:World. E  Type 

latex

Definitions	x:A. B(x), t  T, E, x. t(x), , x(s)
Lemmas	Id wf, nat wf, not wf, assert wf, w-isnull wf, pi1 wf, w-a wf, pi2 wf, world wf